\begin{tabbing}
$\forall$${\it es}$:ES, $T$:Type, $I$:MaInterface($T$), $i$:Id.
\\[0ex]($i$ $\in$ ma{-}interface{-}locs($I$))
\\[0ex]$\Rightarrow$ ma{-}interface{-}consistent2(${\it es}$;$I$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E.\+
\\[0ex]($\uparrow$($e$ $\in_{b}$ [[$I$$\mid$$i$]]))
\\[0ex]$\Rightarrow$ (do{-}apply(ma{-}interface{-}code($I$;$i$;kind($e$))((state when $e$));val($e$)) $\in$ $T$))
\-
\end{tabbing}